Rem(a;n;r) == q:. (Div(a;n;q) & (q * n)+r = a) 

latex

---

clarification:

Rem(a;n;r) == q:. (Div(a;n;q) & (q * n)+r = a  ) 

latex

Up	int 2, int 2
Wellformedness Lemmas	rem nrel wf, rem nrel wf
Definitions	x:A. B(x), , P & Q, Div(a;n;q), s = t, , n+m, n * m
FDL editor aliases	rem_nrel